#include <fstream>
#include <iostream>

#include "input.h"
#include "generalizer.h"
#include "prover.h"
#include "system.h"
#include "try.h"

bool ruleTerminated (std::string &r) {
  return !r.empty () && *(r.end () - 1) == endOfRuleMarker;
}

bool System::load (const std::string &filename) {
  std::string real = trim (filename);
  if(real[0] == '%') // Appends singlog path when referring from home
    real = Input::singlogPath + real.substr (1, std::string::npos);

  std::ifstream is (real.c_str ());
  if(!is)
    return false;

  // Discards first line if we are interpreting as script
  std::string line;
  if(is.peek () == '#')
    getline (is, line);

  bool result = true;
  while(!is.eof ()) {
    bool terminated = false;
    std::string input, pured; // Purify by removing comments

    // Reads a line and check termination symbol
    while(!is.eof () && !terminated) {
      getline (is, line);
      Input::concatLine (input, line);

      // Prevents the line-termination inside comments case
      // (Do not break such comments)
      if(ruleTerminated (input))
        terminated = ruleTerminated (pured = removeComments (input));
    }

    // Process it: assert the rule, or issue the query
    if(!pured.empty ()) {
      std::string::iterator last = pured.end () - 1;
      if(*last == endOfRuleMarker)
        pured.erase (last);
      if(input.length () && !process (pured))
        result = false;
    }
  }

  return result;
}

bool System::process (std::string &input) {
  pNode node;

  std::string query;
  if(input[0] == '?')
    query = input.substr (1);
  if(input.substr (0, 2) == inferenceOperator)
    query = input.substr (2);

  if(query.length ())
    try {
      Trail trail;
      System system (rules, globals, trail);

      node = query;
      node = generalize (*node);
      Prover *prover = Prover::create (*node, system);
      bool result = prover->prove ();
      delete prover;
      return result;
    } catch(RaisedException ex) {
      std::cerr << "[ERROR] Caught exception: " << ex.node.node->dump ()
          << std::endl;
      return false;
    }
  else {
    node = input;
    rules.assertz (node);
    return true;
  }
}
